Инициальность MLTT

Коньюнктура инициальности в теории типов утверждает, что модель термов (все термы и все типы) определенной системы типов должна быть инициальным объектом в категории моделей этой системы типов. Инициальность валидирует формальный переход от теории категории в систему типов, таким образом, что синтаксические пруфтермы системы типов в точности соотвествуют теоремам в категории, которые интерпретируют эти системы типов.

Впервые инициальности для чистых систем (Pure Type Systems), состощих из одного П-типа, была дана Томасом Страйхером в 1991 году. С тех пор инициальность для более сложных типовых систем, как то Martin-Löf Type Theory (MLTT), считалась достигнута, подразумавая механическое продолжение техники категорной формализации для других типов (Σ, Id, +, ⊤, ⊥, N, U_i, El). Хотя многие исследователи, начиная с Владимира Воеводского и его серии статей посвященных важности механистической формализации коньюнктуры инициальности в 2015-2017 гг, занимались исследованиями инициальности, но лишь в 2020 году Гийом Брунери, Питер Люмсдейн совместно с Менно де Боером и Андерсом Мöртбергом представили формальную модель инициальности MLTT на Agda.

Проблема инициальности может выражаться по-разному, сам Страйхер использовал CwF, CwA модели, Воеводский использовал изоморфные C-системы. Тери Кокан же использует предпучковую модель теории типов, где частичные функции выражены как классификаторы подобъектов некоторых топосов, которые репрезентуют и упаковывают модель теориит типов в более подходящем виде, необходимом как для геометрической интерпретации, так и для модальной теории типов (где нужно совершать переход между сопряжениями с помощью функтора изменения базы).

Представленная категорная модель инициальности MLTT Брунери и Люмсдейном является естественным продолжением работы Страйхера и оставляет открытой проблему инициальности в перспективе предпучковые формализаций теории типов. Пару слов об этой модели.

Алгебраическая теория категорий состоит из двух А) сортов: 1) Ob, 2) Mor; Б) морфизмов: 𝛿₀: Mor → Ob (домен) 𝛿₁ : Mor → Ob, (кодомен), id: Ob → Ob, comp: (f g: Mor)(p: 𝛿₀(f)=𝛿₁(g))→ Mor; В) семи уравнений: id₀, id₁, comp₀, comp₁, id-left, id-right, assoc.

Категории контекстов. Для каждой теории типов мы можем построить категорию, где объекты есть выводимые контексты факторизированые по отношению эквивалентности, а морфизмы есть полные подстановки факторизированые по отношению эквивалентности. В этой категории у каждого объекта (контекста) есть длина (словаря переменны в сигма-контексте). В алгебру этой категории вводятся дополнительные операции и их типы. Например вводится операция ft : Ob_n+1 -> Ob_n, которая принимает объект длины n+1 и возвращает контекст предыдущего шага (хвост): ft = \ (Г,A) → Г, который всегда имеет длину n. Таким образом тип А в контексте Г формулируется как объект (Г,А), такой что ft (Г,А) = Г.

Полный набор операций в таких градуированых натуральными числами категориях будет следующий: ft : Ob_n+1 → Ob_n (предыдущий контекст), pp : Ob_n+1 → Mor_n+1,n (проекция на предыдущий), star : (f: Mor_n,n)(X: Ob_n+1)(p: 𝛿 ₁(f) = ft X)) → Ob_n+1 (подстановка), qq : (f: Mor_n,n)(X: Ob_n+1)(p: 𝛿 ₁(f) = ft X)) → Mor_m+1,n+1 (последняя переменная), ss : Mor_m,n+1 → Mor_m,n+1 (последний терм), pt : Ob₀, pt-mor: Ob₀ → Mor_n,0 (пустой контекст) и новых 19 уравнений. Количество сортов становится N ∪ N², все контексты всех размеров, и все морфизмы между контекстами любого размера.